Inference at * 
Iof proof for Lemma p-lift wf:


  A, B:Type, P:(A), d:(x:ADec(P(x))), f:({x:A| P(x)} B). p-lift(d;f)  A(B + Top) 

latex

 by (Unfold `p-lift` ( 0)) 
CollapseTHEN (Auto) 

latex

C1: .....subterm..... T:t1:n

C1: 1. A : Type
C1: 2. B : Type
C1: 3. P : A
C1: 4. d : x:ADec(P(x))
C1: 5. {x:A| P(x)} B
C1: 6. x : A
C1:   d(x)  (P(x) + (P(x)))
C.

Definitions	p-lift(d;f), x.A(x), case b of inl(x) => s(x) | inr(y) => t(y), inl x , inr x , False, P  Q, left + right, A, Top, x:A.B(x), Void, {x:A| B(x)} , Dec(P), x:A. B(x), x(s), f(a), x:AB(x), , t  T, Type
Lemmas	top wf, decidable wf